T:Type, L1,L2:(T List). sublist(T; L1; L2)  prop{i:l} 

latex

Definitions	suptype(S; T), subtype(S; T), P  Q, x:A. B(x), sublist(T; L1; L2), prop{i:l}, t  T, x:A. B(x), P  Q, int_seg(i; j)
Lemmas	select wf, non neg length, increasing wf, length wf1, int seg wf